/* Benchmarks for the PionterC verifier. */

// array index


/*@ i>=0 && i <=10 */
int f(int i)
{
  array[10, int] x, y;
  x[i] = 1;
  x[i] = 1;
  x[i] = 1;
  x[i] = 1;
  x[i] = 1;
  x[10] = 1;
  x[i] = 1;
  return 0;
}
/*@   */